FDL - Nuprl Lemma : rel-immediate-preserves-order

Nuprl Lemma : rel-immediate-preserves-order

T:Type, R:(T

T

).
Trans(T;x,y.R(x,y))

sum_of_torder(T;R)

(

x, y, x', y':T. (R(x,y))

(R!(x',x))

(R!(y',y))

(R(x',y')))

Definitions P Q, R!, sum_of_torder(T;R), Trans(T;x,y.E(x;y)), x:A. B(x), x,y. t(x;y), f(a), x:AB(x), , t T, Type, P Q, s = t, P & Q, A c B, x:A B(x), left + right, SQType(T), {T}, s ~ t

Lemmas rel-immediate-property, trans wf, sum of torder wf, rel-immediate wf